x, y:Top, nms1, nms2:(MaName List).
if nms1 and nms2 overlap then x else y fi ~ if nms2 and nms1 overlap then x else y fi 

latex

Definitions	P  Q, P & Q, P  Q, x:A. B(x), MaName, False, A, s = t, x:AB(x), l_disjoint(T;l1;l2), left + right, P  Q, Dec(P), t  T, , if p:P then A(p) else B fi , if nms1 and nms2 overlap then x else y fi, type List, Top,
Lemmas	l disjoint-symmetry